package org.cos.verifier.automata;

import java.util.Enumeration;
import java.util.Vector;



// Modified by ZXD on 2009.5.9
class Condition{
	public String type = null;
	public int target_id = -1;
	public Vector sets = null;
	public	 Condition(String type, int target_id, Vector sets) {
		this.type = type;
		this.target_id = target_id;
		this.sets = sets;
	}
	
	public Pair intersect(Condition cond) {
		if (type.equals(cond.type) && target_id == cond.target_id) {
			Vector inter_sets = new Vector();
			Vector remain_sets = new Vector();
			for (Enumeration my_e = sets.elements();my_e.hasMoreElements();) {
					CondSet my_set = (CondSet) my_e.nextElement();
				for (Enumeration your_e = cond.sets.elements(); your_e.hasMoreElements();) {
						CondSet your_set = (CondSet) your_e.nextElement();
					Pair unionPair = my_set.intersect(your_set);
					CondSet inter_set = (CondSet) unionPair.head;
					CondSet remain_set = (CondSet) unionPair.tail;
					if (inter_set != null) inter_sets.add(inter_set);
					if (remain_set != null) remain_sets.add(remain_set);
				}
			}
			Condition inter_cond = inter_sets.isEmpty() ? null : new Condition(type, target_id, inter_sets);
			Condition remain_cond = remain_sets.isEmpty() ? null : new Condition(type, target_id, remain_sets);
			return new Pair(inter_cond, remain_cond);
		}
		return null;
	}
	
	public boolean satisfy(Object o) {
		for (Enumeration e = sets.elements();e.hasMoreElements();) {
			CondSet set = (CondSet) e.nextElement();
			if (set.contains(o)) {
				return true;
			}
		}
		return false;
	}
}

// Modified by ZXD on 2009.5.9
class CondSet {

	public String relation = null;
	
	public Object value_u = null;
	public Object value_d = null;
	
	public CondSet(String relation, Object value_u, Object value_d){
		this.relation = relation;
		this.value_u = value_u;
		this.value_d = value_d;
	}
	
	public boolean contains(Object o) {
		if (relation.equals("EQUAL")) {
			if (o.equals(value_u)) return true; 
		}
		return false;
	}
	
	public Pair intersect(CondSet set) {
		if (relation.equals("EQUAL")) {
			if (set.relation.equals("EQUAL")) {
				if (value_u.equals(set.value_u)) {
					return new Pair(this, null);
				} else {
					return new Pair(null, this);
				}
			} else if (set.relation.equals("PREFIX")) {
				String str_value = value_u.toString();
				String str_prefix = set.value_u.toString();
				if (str_value.startsWith(str_prefix)) {
					return new Pair(this, null);
				} else {
					return new Pair(null, this);
				}
			}
		}
		return new Pair(null, this);
	}
}

class Action {
	public String type = null;
	public int target_id = -1;
	public String opt = null;
	public String value = null;
	public Action(String type, int target_id, String opt, String value) {
		this.type = type;
		this.target_id = target_id;
		this.opt = opt;
		this.value = value;
	}	
}

class Method {
	public String name;
	public Vector params_type;
	public Method(String name, Vector params_type) {
		this.name = name;
		this.params_type = params_type;
	}

	
	public String toString() {
		String str = this.name+"(";
		for (Enumeration enumobj = this.params_type.elements(); enumobj.hasMoreElements();) {
			str += (String)enumobj.nextElement() + ",";
		}
		if (str.endsWith(",")) {
			str = str.substring(0, str.length() - 1);
		}
		str += ")";
		return str; 
	}

	public int hashCode() {
		return this.toString().hashCode();
	}
	
	public boolean cmp_method(Method m) {
		boolean diff = true;
		if (! this.name.equals(m.name)) {
			diff = false;
		} 
		for (Enumeration e1 = this.params_type.elements(); e1.hasMoreElements() && diff;) {
			String s1 = (String)e1.nextElement();
			for (Enumeration e2 = m.params_type.elements(); e2.hasMoreElements() && diff;) {
				String s2 = (String)e2.nextElement();
				if (! s1.equalsIgnoreCase(s2)) {
					diff = false;
				}
			}
		}
		return diff;
	}
	
	public boolean equals(Object other) {
		return this.hashCode() == other.hashCode();
	}
	
}


public class Transition {
	public Method method;
	public Vector conditions;
	public Vector actions;
	
	public Transition(Method method,
			Vector conditions, Vector actions) {
		this.method = method;
		this.conditions = conditions;
		this.actions = actions;
	}

	public String toString(){
		return new String(method.toString());
	}
	
}